L: List, a:. 0<||L||  (aimax-list(L)  (bL.ab)) 

latex

Definitions	{T}, imax(a;b), ij, P  Q, P & Q, P  Q, x. t(x), (xL.P(x)), , A, False, P  Q, ||as||, imax-list(L), Prop, P  Q, t  T, AB, x:A. B(x)
Lemmas	le wf, l exists wf, imax ub, or functionality wrt iff, l exists cons, non neg length, length cons, length wf1, false wf, l exists nil, iff functionality wrt iff, imax-list wf, imax wf, length wf2, nat wf, nat properties, ge wf